The majority of modern processors consist of a plurality of processor cores working in parallel. In order to be able to fully utilize the power of such multi-core processors, the applications that are to be executed on them must be parallelized.
The development of parallel software is, however, highly subject to errors, especially since it is very difficult to maintain an overview of the large number of different flow scenarios in one parallel program.
Typical faults in programs that are running in parallel or concurrently are:                deadlocks which can lead to the system locking up through circular dependencies between a plurality of threads        race conditions, which always occur when a plurality of threads access common data without synchronization.        
Race conditions can have the following causes here:                atomicity violations, in which an operation has only partially been executed and is interrupted by another operation before it has completed.        order violations in which the intended sequence of a plurality of operations is not maintained as a result of optimizations made by the compiler or processor.        visibility violations, in which the result of one operation is not immediately written back into the main memory, and is therefore invisible for other threads.        
A simple example of atomicity violations is the incrementation of an integer variable. Three steps are usually necessary for this: reading the current value from the memory, adding one, and saving the new value. If these three steps are not executed atomically, it can happen that changes to the variable are lost (lost updates).
Special methods and tools which allow the correctness of programs running in parallel to be checked are required to avoid such errors. Classical methods such as testing and debugging are not, however, adequate for this purpose.
A variety of tools and methods exist which assist the discovery of faults in parallel programs. Dynamic analysis methods, wherein the program to be investigated is executed and examined for race situations, deadlocks and so forth, are the most common.
Examples of such tools include the Intel® Inspector, the Oracle Thread Analyzer, Helgrind/DRD and ThreadSanitizer. These known tools are, however, all restricted to relatively simple faults. It is not, however, possible to check more complex properties such as invariants with them, where an invariant refers to a property that must always be satisfied in a particular section of the program. A further disadvantage of these approaches is that they are typically not employed until the program to be developed is already largely finished.
As in the case of sequential programming, it is more helpful to stipulate properties in the program code by means of assertions as early as the development stage. Such an approach is described in D. Schwartz-Narbonne, F. Liu, T. Pondicherry, D. August, S. Malik, “Parallel Assertions for Debugging Parallel Programs. Formal Methods and Models for Codesign (MEMOCODE' 11), IEEE 2011. This approach also, however, is restricted to relatively simple properties, and does not allow the specification of arbitrary invariants. It also requires a modification to the compiler, which, however, heavily restricts its practical application.